_ORG1_ =
    {privkey=<RSAKeyValue><Modulus>kUWXmVPrxaQBAE+hxwzlzo/+hOTL60RIa2O+Ud0vnUUTB0OO+znVakY2dXnW/hqMa7cx49GCUFUx7iTv4cFYHPtAzFecyrbIzwLBdhbcATj2qpRVsrSoBtVRxEAqiktil5IhtCk7usy85HYDxNbVw/HWHvQRTd6cuYnKb4KNU1E=</Modulus><Exponent>AQAB</Exponent><P>xq4lK+sSdwEB1fCcyW5wQKfx74TWx+uxXjHunyXDKZhgkNiZ685VWr1kuiCfil2jOp8Hc/9WnlxcdH1nGvQXiQ==</P><Q>uy7hr+TXGQDNXyrje4MOIR9ZAlN1Oz5henc5IKBn+ddqlUQKH9rIqI/PQgBvT44bnnybBr2DiStafB9Hbs0jiQ==</Q><DP>xMnelZabznWX7OELWtThqJjwoM5Rsul34BXTBZ1wpjWAiFeSdacEkgD/0P/ZJkLDF6BG0JU7pVVUWimPw3m8CQ==</DP><DQ>hGb8AuQ29huoKXn34QTpuKoo1slb8iUE5JBym057XbFvVdgD5VZnezwGGaSfF8HobWmsas8gvKUq4wNpDsoSKQ==</DQ><InverseQ>nRitOmPpVe1vKg3Qq1+2SpCOlKxbfEED22CkRJxLVj8ElX0foB38RNJhHxnPvCAEvGdXVRLdeA4N5/nqU/pNyA==</InverseQ><D>N06ue+KWdeWNuAeZSQYhC/aIaSIOfOC/TZto3xP9x7t/lhlje0Q2e0KGA03Cy3ViFrRlWx3tphX5b3hCl8mbeMJLeOk8RFAWHVe3IpKr3Op+D8P2SD20/UopC4RaMlwsNSW++7a2ldifHCobZTwIAK68eR1cSL3gUt/sqnZOhcE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>kUWXmVPrxaQBAE+hxwzlzo/+hOTL60RIa2O+Ud0vnUUTB0OO+znVakY2dXnW/hqMa7cx49GCUFUx7iTv4cFYHPtAzFecyrbIzwLBdhbcATj2qpRVsrSoBtVRxEAqiktil5IhtCk7usy85HYDxNbVw/HWHvQRTd6cuYnKb4KNU1E=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6301}

and _SITE1_ = 
    {privkey=<RSAKeyValue><Modulus>w82NXJIdeCJnm9vNadVHErCaRkoCfU8pap6LDw6N27yHRTTcQcTYZD27D20Nsji21cljjhhpefocP3sa6zeI+VjgtWBB16axdh3eROyyC/1vpS8Q2TIraBrp6Ew8ld51/p35tu5HZhuzN2gltgSTrzsMOvNGfz4HIVUt+DjuDDk=</Modulus><Exponent>AQAB</Exponent><P>8odIOrLxHyb6lbh5qXd+BBMMOo0BDbH+W/B39y3+2YmSEb3uHhpUA+lrf3bMf0BXLRw695nUtWpC6b+sgo3pZQ==</P><Q>zq3XI8r6y2lwHTddCmczOWYL8oCz+z8t9Jf9/LPg+IN8HnYFxRy5ICLNzx0dgG3WaC4wjpk/royFQ3WTQqVURQ==</Q><DP>0jumxwtarPBzA9oXzGlCmXGRhie4pBCJN1VqCKCcbCIutqZ3hSy5a3KptqJafmxdpUL1crCsjF4ChvGaLsmpaQ==</DP><DQ>qot6jveMsdNEh2dK6C22cDPLwgT//1/oDQBqvl60Un01K3GaW0fTXzg4+iH9WR/Jn9gVi2Xbza34vWzE4mbIvQ==</DQ><InverseQ>0ZcWjOdE2Z3F9fdluvKeerIezF/3gzTmdHd9CYwPK/sIuEFP3tF0jzzJxGKFybxaGq0RYcnkkw74LwXSVOsJaw==</InverseQ><D>LkwECMdjwGwiI3AtecC8NWcck1IclJSLLnKeXskKMdK6CVseWU65+7m86UDX5DQUxyf/KjILfpPs6fWpv8Q51pE+ORHhyXOKPLDj/5vgHa0WFvFK3NoCsvB/ahIKINF+XpsWD7AmBWNJUPuqxZrCyYzv7qPT24gEJZCV9scmfIE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>w82NXJIdeCJnm9vNadVHErCaRkoCfU8pap6LDw6N27yHRTTcQcTYZD27D20Nsji21cljjhhpefocP3sa6zeI+VjgtWBB16axdh3eROyyC/1vpS8Q2TIraBrp6Ew8ld51/p35tu5HZhuzN2gltgSTrzsMOvNGfz4HIVUt+DjuDDk=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6302}

and _PHYS1_ =
    {privkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent><P>/rEL5XxETzzYLznPHnFOOHCH+q/61GyB5XY/rWO5kEQygx+wOJNpwZ4F453/v8dTg5epedz4DDlAeJ23LUNjiQ==</P><Q>57oTxICOcOQ6Y0Poaw6vyBwcCHViQMZBBuJH34rUeAmkaG/EG44M51dZ1Y7ictYVI8uoU7d+/59KiGeRhcSv/w==</Q><DP>idQyBeyr4t2geF4mcekLVYvAaq+VZCOcYBsP9rtDDol5dHBPoy5TSw5DTZyRbK1nyozmkCY+rg7FjwB6wqn3UQ==</DP><DQ>ISX2M/Lr7WxIifCp676jGK4kuHUKRBfYL4LpIyo58J34fdQXKpXsdJ+DQ1B4RlMnnQJCJw+lxC1mPRMLtyYGww==</DQ><InverseQ>JChw7RjvCI7B9w1XBEvEoO+87RX4n/uuAnHFa2deRLLht7HN9XAibConnUcSWuHl1CJnCmhsqniR7ds90oigeQ==</InverseQ><D>kC90Rx2+7FEFtEkg9xbEXoVWSUbJk2OfX6z7I5ZYHyRq0TaC0LWXtyqTx+171axB1Oxs8c1+czmAucOM0tKsgeLK+v+fAv9yioU2eYSu+VfSwfZoUgtxVyqXuDOmujE6QU8grtMej1qR4MMytrafBGlWcYEXFo9vmWIsVmIROkE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6303}

and _KEYMGR_ =
    {privkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent><P>/rEL5XxETzzYLznPHnFOOHCH+q/61GyB5XY/rWO5kEQygx+wOJNpwZ4F453/v8dTg5epedz4DDlAeJ23LUNjiQ==</P><Q>57oTxICOcOQ6Y0Poaw6vyBwcCHViQMZBBuJH34rUeAmkaG/EG44M51dZ1Y7ictYVI8uoU7d+/59KiGeRhcSv/w==</Q><DP>idQyBeyr4t2geF4mcekLVYvAaq+VZCOcYBsP9rtDDol5dHBPoy5TSw5DTZyRbK1nyozmkCY+rg7FjwB6wqn3UQ==</DP><DQ>ISX2M/Lr7WxIifCp676jGK4kuHUKRBfYL4LpIyo58J34fdQXKpXsdJ+DQ1B4RlMnnQJCJw+lxC1mPRMLtyYGww==</DQ><InverseQ>JChw7RjvCI7B9w1XBEvEoO+87RX4n/uuAnHFa2deRLLht7HN9XAibConnUcSWuHl1CJnCmhsqniR7ds90oigeQ==</InverseQ><D>kC90Rx2+7FEFtEkg9xbEXoVWSUbJk2OfX6z7I5ZYHyRq0TaC0LWXtyqTx+171axB1Oxs8c1+czmAucOM0tKsgeLK+v+fAv9yioU2eYSu+VfSwfZoUgtxVyqXuDOmujE6QU8grtMej1qR4MMytrafBGlWcYEXFo9vmWIsVmIROkE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6304}

and Init of int
and Hello of int
and SiteParticipates of (prin, int)
and SiteAllocatedPatients of (prin, int, int, int)
and PhysParticipates of (prin, int, prin)
and PhysAllocatedPatients of (prin, int, int, int, prin)
and RequestToRead of (prin, int)
and MayRead of (prin, int)
and KeyForRecord of (prin, int, int)
and Record of (int, int, int, string)
and Trial of (int, prin, string)
and BasicLeq of (int, int)
and InRange of (int, int, int)
and SiteAssignment of (prin, int, int, int)
and PhysAssignment of (prin, int, int, int)
and PhysPatients of (int, string)
and Key of (int, int)
and $let checkRange (vi:string) (vlo:string) (vhi:string) (env:substitution): term =
  let _ = println (strcat "starting checkRange ..." 
                  (strcat vi 
				  (strcat ", " 
                  (strcat vlo
				  (strcat ", "
				  vhi))))) in
  let _ = println (strcat " env ..." (string_of_any_for_coq env)) in
				 
  match (lookupName env vi Int32), (lookupName env vlo Int32), (lookupName env vhi Int32) with
    | Some (Const (Int i)), Some (Const (Int lo)), Some (Const (Int hi)) ->
        let _ = println (strcat "checkrange: " (strcat vi (strcat " = " (string_of_any i)))) in
        let _ = println (strcat "checkrange: " (strcat vlo (strcat " = " (string_of_any lo)))) in
        let _ = println (strcat "checkrange: " (strcat vhi (strcat " = " (string_of_any hi)))) in
	  if intCheckRange i lo hi then App EmptyInfon []
	  else App FalseInfon []
	| _ -> 
            let _ = println (strcat "checkrange ... bad env: " (string_of_any_for_coq env)) in
              App FalseInfon []
	$
